\begin{tabbing}
$\forall$${\it the\_es}$:ES, $e$:E, $l$:IdLnk, $m$:Msg.
\\[0ex]($m$ $\in$ sends($l$;$e$))
\\[0ex]$\Rightarrow$ \=$\exists$${\it e'}$:rvc($l$,mtag($m$),$v$).($e$ $<$ ${\it e'}$)\+
\\[0ex]\& ((msgtype($m$) = valtype(${\it e'}$) $\in$ Type) c$\wedge$ ($v$ = mval($m$) $\in$ valtype(${\it e'}$)))
\-
\end{tabbing}